Section: New Results

Deductive Verification

A bit-vector library for deductive verification.

C. Fumex and C. Marché developed a new library for bit-vectors, in Why3 and SPARK. This library is rich enough for the formal specification of functional behavior of programs that operate at the level of bits. It is also designed to exploit efficiently the support for bit-vectors built-in in some SMT solvers. This work is done in the context of the ProofInUse joint laboratory. The SPARK front-end of Why3, for the verification of Ada programs, is extended to exploit this new bit-vector theory. Several cases studies are conducted: efficient search for rightmost bit of a bit-vector, efficient computation of the number of bits set to 1, efficient solving of the $n$-queens problem. At the level of SPARK, a program inspired from some industrial code (originally developed in C par J. Gerlach, Fraunhofer FOKUS Institute, Germany and partially proved with Frama-C and Coq) is specified in SPARK and proved with automatic solvers only. A paper on that library together with the way it is connected with the built-in support for bitvectors in SMT solver was presented at the NASA Formal methods Conference [24]. The support for bit-vectors is distributed with SPARK since 2015, and SPARK users already reported that several verification conditions, that couldn't be proved earlier, are now proved automatically.

Counterexamples from proof failures.

D. Hauzar and C. Marché worked on counterexample generation from failed proof attempts. They designed a new approach for generating potential counterexamples in the deductive verification setting, and implemented in Why3. When the logic goal generated for a given verification condition is not shown unsatisfiable by an SMT solvers, some solver can propose a model. By carefully reverting the transformation chain (from an input program through the VC generator and the various translation steps to solvers), this model is turned into a potential counterexample that the user can exploit to analyze why its original code is not proved. The approach is implemented in the chain from Ada programs through SPARK, Why3, and SMT solvers CVC4 and Z3. This work is described in a research report [35] and a paper was rpesented at the SEFM Conference [25]. The work on the implementation was continued by S. Dailler. It was considered robust enough to be distributed in the release Pro 16 of SPARK.

Static versus dynamic verification.

C. Marché, together with Y. Moy from AdaCore, J. Signoles and N. Kosmatov from CEA-LIST, wrote a survey paper about the design of the specification languages of Why3 and its front-ends Frama-C and SPARK. The choices made when designing these specification languages differ significantly, in particular with respect to the executability of specifications. The paper reviews these differences and the issues that result from these choices. The paper also emphasizes two aspects where static and dynamic aspects of the specifications play an important role: the specific feature of ghost code, and the techniques that help users understand why static verification fails. This paper was presented at the Isola Symposium [26].

Higher-Order Representation Predicates.

A. Charguéraud investigated how to formalize in Separation Logic representation predicates for describing mutable container data structures that store mutable elements that are themselves described using representation predicates. (In Separation Logic, representation predicates are used to describe mutable data structures, by establishing a relationship between the entry point of the structure, the piece of heap over which this structure spans, and the logical model associated with the structure.) The solution proposed, based on “higher-order representation predicates”, allows for concise specifications of such containers. A. Charguéraud has published a paper presenting, through a collection of practical examples, solutions to the challenges associated with verification proofs based on higher-order representation predicates [19].

Temporary Read-Only Permissions for Separation Logic

A. Charguéraud and François Pottier (Inria Paris) have developed an extension of Separation Logic with temporary read-only permissions. This mechanism allows to temporarily convert any assertion (or “permission”) to a read-only form. Unlike with fractional permissions, no accounting is required: the proposed read-only permissions can be freely duplicated and discarded. Where mutable data structures are temporarily accessed only for reading, the proposed read-only permissions enable more concise specifications and proofs. All the metatheory is verified in Coq. An article has been submitted to a conference [20].

Reasoning About Iteration.

J.-C. Filliâtre and M. Pereira proposed a new approach to the problem of specifying iteration, verifying iterators (such as cursors or higher-order functions), and using iterators. The idea is to characterize the sequence of elements enumerated so far, and only those. The proof methodology is modular, iterator implementations and clients being verified independently of each other. The proposed method is validated experimentally in Why3. This work has been published first at JFLA 2016 [33] and then at NFM 2016 [22]. A journal version of this work is under submission.

Defunctionalization for proving higher-order programs.

J.-C. Filliâtre and M. Pereira proposed a new approach to the verification of higher-order programs, using the technique of defunctionalization, that is, the translation of first-class functions into first-order values. This is an early experimental work, conducted on examples only within the Why3 system. This work has been published at JFLA 2017 [30].

A Type System for Deductive Verification.

J.-C. Filliâtre, L. Gondelman, and A. Paskevich proposed a practical method to track pointer aliases statically in a large family of computer programs. Their approach relies on a special type system with singleton regions and effects which both can be inferred automatically, without requiring additional user annotations. This kind of static analysis is important for deductive program verification, since it allows us to construct verification conditions using the traditional rules in the spirit of Hoare and Dijkstra, without recurring to more sophisticated solutions (memory models, separation logic) which incur additional complexity both for a user and a verification tool. The proposed method is implemented in Why3 and described in a technical report [37].

Ghost Code.

J.-C. Filliâtre, L. Gondelman, and A. Paskevich published a paper on a general approach to the concept of ghost code in the journal of Formal Methods in System Design [14]. Ghost code is a subset of program code that serves the purposes of specification and verification: it can be erased from the program without affecting its result. This work forms the basis of the support for ghost code in Why3. This work is an extended version of the paper presented at the 26th International Conference on Computer Aided Verification (CAV) in 2014.